\begin{tabbing}
es{-}rcv{-}from(${\it es}$;$e$;$l$;$L$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$${\it e'}$:es{-}E(${\it es}$).\+\+
\\[0ex](${\it e'}$ $\in$ $L$ $\in$ es{-}E(${\it es}$))
\\[0ex]$\Leftrightarrow$
\\[0ex]es{-}isrcv(${\it es}$; ${\it e'}$) \& es{-}lnk(${\it es}$; ${\it e'}$) $=$ $l$ $\in$ IdLnk \& es{-}sender(${\it es}$; ${\it e'}$) $=$ $e$ $\in$ es{-}E(${\it es}$))
\-\\[0ex]\& ($\forall$$e_{1}$:es{-}E(${\it es}$), $e_{2}$:es{-}E(${\it es}$). $e_{1}$ before $e_{2}$ $\in$ $L$ $\in$ es{-}E(${\it es}$) $\Rightarrow$ es{-}locl(${\it es}$; $e_{1}$; $e_{2}$))
\-
\end{tabbing}